imax(a;b) == if a z b then b else a fi  

latex

Up	int 2, int 2
Wellformedness Lemmas	imax wf, imax wf
Definitions	if b then t else f fi , i z j
FDL editor aliases	imax